_require local "../../../../basis.smi"

_require "../../../data/symbols/main/Loc.smi"
_require local "../../../data/symbols/main/RecordLabel.smi"
_require local "../../../extensions/debug/main/Bug.smi"
_require local "../../../libs/ids/main/LocalID.smi"
(* _require local "../../../libs/env/main/SEnv.smi" *)
_require local "../../../data/builtin/main/BuiltinTypes.smi"

_require "../../../compilerIRs/typedcalc/main/TypedCalc.ppg.smi"
_require local "../../../compilerIRs/typedcalc/main/TypedCalcUtils.smi"
_require "../../../data/types/main/Types.ppg.smi"
_require local "../../../data/types/main/TypesBasics.smi"
_require local "../../../data/types/main/Unify.smi"
_require local "./Printers.smi"

structure TypeInferenceUtils =
  struct
(*
    val nextDummyTy : Types.kind -> Types.ty
*)
    val freshTopLevelInstTy : Types.ty -> Types.ty * Types.ty list option * Types.constraint list
    val instantiateOConstTy : Types.ty -> unit
    val instantiateOConstAndRecordTy : Types.ty -> bool

(*
    val eliminateVacuousTyvars : unit -> unit

    exception NONEQ
    val eqTy : BoundTypeVarID.id BoundTypeVarID.Map.map
               -> Types.ty * Types.ty -> bool
    val eqSMap : BoundTypeVarID.id BoundTypeVarID.Map.map
                 -> Types.ty RecordLabel.Map.map * Types.ty RecordLabel.Map.map -> bool
    val eqTyList : BoundTypeVarID.id BoundTypeVarID.Map.map
                   -> Types.ty list * Types.ty list -> bool
    val eqSTy : BoundTypeVarID.id BoundTypeVarID.Map.map
                -> Types.singletonTy * Types.singletonTy -> bool
    val eqOprimSelector
        : BoundTypeVarID.id BoundTypeVarID.Map.map
          -> Types.oprimSelector * Types.oprimSelector -> bool
    val eqOprimSelectorList
        : BoundTypeVarID.id BoundTypeVarID.Map.map
          -> Types.oprimSelector list * Types.oprimSelector list
          -> bool
    val eqKind : BoundTypeVarID.id BoundTypeVarID.Map.map
                 -> {eqKind:Types.eq, tvarKind:Types.tvarKind}
                    * {eqKind:Types.eq, tvarKind:Types.tvarKind}
                 -> bool
    val eqTvarKind : BoundTypeVarID.id BoundTypeVarID.Map.map
                     -> Types.tvarKind * Types.tvarKind -> bool
*)
    exception CoerceTy
    val coerceTy : TypedCalc.tpexp * Types.ty * Types.ty * Loc.loc
                   -> {tpexp:TypedCalc.tpexp, constraints:Types.constraint list}
  end
